Cairo VMの論文

本論文では、証明された計算を表現するという課題に対して、

計算をコンピュータプログラムの形で記述し、その計算の完全性の証明を生成できるアーキテクチャであるCairo(システムの名前でもあり、固有の言語の名前でもある)を導入することで、この課題に取り組む。

Cairoアーキテクチャは次のような目的で設計されている。

(1)証明可能なステートメントとして使用するプログラムの記述と読み込みが容易であること。

(2)STARKをベースとした効率的な証明

既存の実用的な証明システムの多くでは、証明される計算を表すために計算を有限体上の多項式で表現する必要がある。

この処理は「arithmetization:算術化」と呼ばれる．

算術化の例としてはQuadratic Span Programs (別名R1CS)、Algebraic Intermediate Representations (AIRs)などがある

このように、計算を多項式で表現する必要があるため、これらの証明体系を実用化することは非常に困難である。

また、演算処理のアプローチによっては、無駄な計算が発生する。

例:x ≠ y のassert

多項式は通常、p = 0（p≠0ではない）の形式でなければならないことに注意してください。

p は変数の多項式である。

x ≠ y という主張は ∃ (x - y) - a = 1 (補助変数 a を追加する) に変換できる。

少し複雑な2^64の足し算は、和の2値表現を捕らえる64の補助変数を加えることで、多項式に変換することができる。

この作業は，計算の分岐（例えば，x = yならある処理を行い，そうでなければ別の処理を行う）やループ（例えば，x = yになるまで処理を繰り返す）を扱わなければならなくなるとさらに複雑になる．

分岐を処理する方法の1つは、分岐の両方を多項式に変換し、条件の値に応じて結果を「選択」する式を1つ加えることである（例えば、式z = (1-b)-x+b-y は、b = 0ならz = x、b = 1ならz = yと強制するものである）。

ループは次のように処理することができる。ループは、反復の回数をある定数Bで制限し、ループの本体をちょうどB回実行することで、対処できます。ループは、ループの本体を正確にB回実行し、ある時点で条件を満たした場合 ある時点で条件が満たされた場合、次の反復は単にループの終わりまで結果を渡すだけである。ループの終わりまで結果を渡すだけです。

最後の2つのケースでは、さらに「不要な」計算が必要であることに注意してください。最初のケースでは2つの分岐を実行し、2番目のケースではループが早期に終了してもB回の反復計算を実行します。

計算の表現の課題(challenges of the computation’s representation)に対処するアプローチ

1. コンパイラを作る

つまりコードを入力として受け取り、コードの実行を表す多項式リストを出力するプログラム

ZKPDL 、Pinocchio、SNARKsとSTARKsのためのTinyRAM、xJsnarkなど

プログラムを単純化する一方で不要なコードを実行する非効率性やループの反復回数を制限する必要性がある

2.CPUの発明とノイマン型コンピュータに頼る

ある固定された命令セットに対して書かれた任意のコンピュータプログラムの実行を表す多項式からなる単一の普遍的な系を設計することができる。

SNARKの前処理の文脈では、このアプローチはvnTinyRAMシステムで使用されています